↳ Prolog
↳ PrologToPiTRSProof
normal_in_ga(F, N) → U1_ga(F, N, rewrite_in_ga(F, F1))
rewrite_in_ga(op(op(A, B), C), op(A, op(B, C))) → rewrite_out_ga(op(op(A, B), C), op(A, op(B, C)))
rewrite_in_ga(op(A, op(B, C)), op(A, L)) → U3_ga(A, B, C, L, rewrite_in_ga(op(B, C), L))
U3_ga(A, B, C, L, rewrite_out_ga(op(B, C), L)) → rewrite_out_ga(op(A, op(B, C)), op(A, L))
U1_ga(F, N, rewrite_out_ga(F, F1)) → U2_ga(F, N, normal_in_ga(F1, N))
normal_in_ga(F, F) → normal_out_ga(F, F)
U2_ga(F, N, normal_out_ga(F1, N)) → normal_out_ga(F, N)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
normal_in_ga(F, N) → U1_ga(F, N, rewrite_in_ga(F, F1))
rewrite_in_ga(op(op(A, B), C), op(A, op(B, C))) → rewrite_out_ga(op(op(A, B), C), op(A, op(B, C)))
rewrite_in_ga(op(A, op(B, C)), op(A, L)) → U3_ga(A, B, C, L, rewrite_in_ga(op(B, C), L))
U3_ga(A, B, C, L, rewrite_out_ga(op(B, C), L)) → rewrite_out_ga(op(A, op(B, C)), op(A, L))
U1_ga(F, N, rewrite_out_ga(F, F1)) → U2_ga(F, N, normal_in_ga(F1, N))
normal_in_ga(F, F) → normal_out_ga(F, F)
U2_ga(F, N, normal_out_ga(F1, N)) → normal_out_ga(F, N)
NORMAL_IN_GA(F, N) → U1_GA(F, N, rewrite_in_ga(F, F1))
NORMAL_IN_GA(F, N) → REWRITE_IN_GA(F, F1)
REWRITE_IN_GA(op(A, op(B, C)), op(A, L)) → U3_GA(A, B, C, L, rewrite_in_ga(op(B, C), L))
REWRITE_IN_GA(op(A, op(B, C)), op(A, L)) → REWRITE_IN_GA(op(B, C), L)
U1_GA(F, N, rewrite_out_ga(F, F1)) → U2_GA(F, N, normal_in_ga(F1, N))
U1_GA(F, N, rewrite_out_ga(F, F1)) → NORMAL_IN_GA(F1, N)
normal_in_ga(F, N) → U1_ga(F, N, rewrite_in_ga(F, F1))
rewrite_in_ga(op(op(A, B), C), op(A, op(B, C))) → rewrite_out_ga(op(op(A, B), C), op(A, op(B, C)))
rewrite_in_ga(op(A, op(B, C)), op(A, L)) → U3_ga(A, B, C, L, rewrite_in_ga(op(B, C), L))
U3_ga(A, B, C, L, rewrite_out_ga(op(B, C), L)) → rewrite_out_ga(op(A, op(B, C)), op(A, L))
U1_ga(F, N, rewrite_out_ga(F, F1)) → U2_ga(F, N, normal_in_ga(F1, N))
normal_in_ga(F, F) → normal_out_ga(F, F)
U2_ga(F, N, normal_out_ga(F1, N)) → normal_out_ga(F, N)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
NORMAL_IN_GA(F, N) → U1_GA(F, N, rewrite_in_ga(F, F1))
NORMAL_IN_GA(F, N) → REWRITE_IN_GA(F, F1)
REWRITE_IN_GA(op(A, op(B, C)), op(A, L)) → U3_GA(A, B, C, L, rewrite_in_ga(op(B, C), L))
REWRITE_IN_GA(op(A, op(B, C)), op(A, L)) → REWRITE_IN_GA(op(B, C), L)
U1_GA(F, N, rewrite_out_ga(F, F1)) → U2_GA(F, N, normal_in_ga(F1, N))
U1_GA(F, N, rewrite_out_ga(F, F1)) → NORMAL_IN_GA(F1, N)
normal_in_ga(F, N) → U1_ga(F, N, rewrite_in_ga(F, F1))
rewrite_in_ga(op(op(A, B), C), op(A, op(B, C))) → rewrite_out_ga(op(op(A, B), C), op(A, op(B, C)))
rewrite_in_ga(op(A, op(B, C)), op(A, L)) → U3_ga(A, B, C, L, rewrite_in_ga(op(B, C), L))
U3_ga(A, B, C, L, rewrite_out_ga(op(B, C), L)) → rewrite_out_ga(op(A, op(B, C)), op(A, L))
U1_ga(F, N, rewrite_out_ga(F, F1)) → U2_ga(F, N, normal_in_ga(F1, N))
normal_in_ga(F, F) → normal_out_ga(F, F)
U2_ga(F, N, normal_out_ga(F1, N)) → normal_out_ga(F, N)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
REWRITE_IN_GA(op(A, op(B, C)), op(A, L)) → REWRITE_IN_GA(op(B, C), L)
normal_in_ga(F, N) → U1_ga(F, N, rewrite_in_ga(F, F1))
rewrite_in_ga(op(op(A, B), C), op(A, op(B, C))) → rewrite_out_ga(op(op(A, B), C), op(A, op(B, C)))
rewrite_in_ga(op(A, op(B, C)), op(A, L)) → U3_ga(A, B, C, L, rewrite_in_ga(op(B, C), L))
U3_ga(A, B, C, L, rewrite_out_ga(op(B, C), L)) → rewrite_out_ga(op(A, op(B, C)), op(A, L))
U1_ga(F, N, rewrite_out_ga(F, F1)) → U2_ga(F, N, normal_in_ga(F1, N))
normal_in_ga(F, F) → normal_out_ga(F, F)
U2_ga(F, N, normal_out_ga(F1, N)) → normal_out_ga(F, N)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
REWRITE_IN_GA(op(A, op(B, C)), op(A, L)) → REWRITE_IN_GA(op(B, C), L)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
REWRITE_IN_GA(op(A, op(B, C))) → REWRITE_IN_GA(op(B, C))
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
NORMAL_IN_GA(F, N) → U1_GA(F, N, rewrite_in_ga(F, F1))
U1_GA(F, N, rewrite_out_ga(F, F1)) → NORMAL_IN_GA(F1, N)
normal_in_ga(F, N) → U1_ga(F, N, rewrite_in_ga(F, F1))
rewrite_in_ga(op(op(A, B), C), op(A, op(B, C))) → rewrite_out_ga(op(op(A, B), C), op(A, op(B, C)))
rewrite_in_ga(op(A, op(B, C)), op(A, L)) → U3_ga(A, B, C, L, rewrite_in_ga(op(B, C), L))
U3_ga(A, B, C, L, rewrite_out_ga(op(B, C), L)) → rewrite_out_ga(op(A, op(B, C)), op(A, L))
U1_ga(F, N, rewrite_out_ga(F, F1)) → U2_ga(F, N, normal_in_ga(F1, N))
normal_in_ga(F, F) → normal_out_ga(F, F)
U2_ga(F, N, normal_out_ga(F1, N)) → normal_out_ga(F, N)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
NORMAL_IN_GA(F, N) → U1_GA(F, N, rewrite_in_ga(F, F1))
U1_GA(F, N, rewrite_out_ga(F, F1)) → NORMAL_IN_GA(F1, N)
rewrite_in_ga(op(op(A, B), C), op(A, op(B, C))) → rewrite_out_ga(op(op(A, B), C), op(A, op(B, C)))
rewrite_in_ga(op(A, op(B, C)), op(A, L)) → U3_ga(A, B, C, L, rewrite_in_ga(op(B, C), L))
U3_ga(A, B, C, L, rewrite_out_ga(op(B, C), L)) → rewrite_out_ga(op(A, op(B, C)), op(A, L))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
NORMAL_IN_GA(F) → U1_GA(rewrite_in_ga(F))
U1_GA(rewrite_out_ga(F1)) → NORMAL_IN_GA(F1)
rewrite_in_ga(op(op(A, B), C)) → rewrite_out_ga(op(A, op(B, C)))
rewrite_in_ga(op(A, op(B, C))) → U3_ga(A, rewrite_in_ga(op(B, C)))
U3_ga(A, rewrite_out_ga(L)) → rewrite_out_ga(op(A, L))
rewrite_in_ga(x0)
U3_ga(x0, x1)
rewrite_in_ga(op(op(A, B), C)) → rewrite_out_ga(op(A, op(B, C)))
POL(NORMAL_IN_GA(x1)) = x1
POL(U1_GA(x1)) = x1
POL(U3_ga(x1, x2)) = 1 + 2·x1 + x2
POL(op(x1, x2)) = 1 + 2·x1 + x2
POL(rewrite_in_ga(x1)) = x1
POL(rewrite_out_ga(x1)) = x1
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
NORMAL_IN_GA(F) → U1_GA(rewrite_in_ga(F))
U1_GA(rewrite_out_ga(F1)) → NORMAL_IN_GA(F1)
rewrite_in_ga(op(A, op(B, C))) → U3_ga(A, rewrite_in_ga(op(B, C)))
U3_ga(A, rewrite_out_ga(L)) → rewrite_out_ga(op(A, L))
rewrite_in_ga(x0)
U3_ga(x0, x1)
U1_GA(rewrite_out_ga(F1)) → NORMAL_IN_GA(F1)
U3_ga(A, rewrite_out_ga(L)) → rewrite_out_ga(op(A, L))
POL(NORMAL_IN_GA(x1)) = 1 + 2·x1
POL(U1_GA(x1)) = 1 + x1
POL(U3_ga(x1, x2)) = 2·x1 + 2·x2
POL(op(x1, x2)) = x1 + 2·x2
POL(rewrite_in_ga(x1)) = 2·x1
POL(rewrite_out_ga(x1)) = 1 + 2·x1
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
NORMAL_IN_GA(F) → U1_GA(rewrite_in_ga(F))
rewrite_in_ga(op(A, op(B, C))) → U3_ga(A, rewrite_in_ga(op(B, C)))
rewrite_in_ga(x0)
U3_ga(x0, x1)